Step of Proof: p-conditional-to-p-first 11,40
Inference at * 
Iof proof for Lemma p-conditional-to-p-first:


  A, B:Type, f, g:(A(B + Top)). [f?g] = p-first([f; g]) 
latex
 by ((Auto) 
CollapseTHEN (((Ext) 
CollapseTHEN (Auto)))) 
latex

C1: 

C1: 1. A : Type
C1: 2. B : Type
C1: 3. f : A(B + Top)
C1: 4. g : A(B + Top)
C1: 5. x : A
C1:   [f?g](x) = p-first([f; g])(x)
C.

Definitions[f?g], Type, p-first(L), [car / cdr], x:A. B(x), s = t, A List, t  T, [], type List, x:AB(x), left + right, Top
Lemmasp-conditional wf, p-first wf, top wf

origin